Propel: Automated Verification of CRDTs and Fundamental Algebraic Laws
Propel is a functional programming language and verifier that allows programmers to annotate their functions with certain algebraic properties such as commutativity, associativity, and idempotency. These "algebraic laws" have several useful applications in functional programming (e.g. when implementing CRDTs) and can be used to reason about the correctness of a piece of code. Using the annotations, propel can automatically verify if the desired laws hold for the given program.
For this seminar topic, you will explore the core ideas of Propel and explain its design along with challenges and limitations in you seminar paper. Additionally, you will try out the Propel language yourself to see if you can implement and verify a small program.